0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 88 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 0 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 18 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 PiDP
↳9 PiDPToQDPProof (⇒, 5 ms)
↳10 QDP
↳11 QDPSizeChangeProof (⇔, 11 ms)
↳12 YES
conB_in_g(and(or(T14, T15), T5)) → U4_g(T14, T15, T5, conB_in_g(T14))
conB_in_g(and(T57, T5)) → U7_g(T57, T5, conB_in_g(T57))
conB_in_g(0) → conB_out_g(0)
conB_in_g(1) → conB_out_g(1)
U7_g(T57, T5, conB_out_g(T57)) → conB_out_g(and(T57, T5))
U7_g(T57, T5, conB_out_g(T57)) → U8_g(T57, T5, conB_in_g(T5))
U8_g(T57, T5, conB_out_g(T5)) → conB_out_g(and(T57, T5))
U4_g(T14, T15, T5, conB_out_g(T14)) → conB_out_g(and(or(T14, T15), T5))
U4_g(T14, T15, T5, conB_out_g(T14)) → U5_g(T14, T15, T5, disA_in_g(T15))
disA_in_g(or(T32, T33)) → U1_g(T32, T33, conB_in_g(T32))
U1_g(T32, T33, conB_out_g(T32)) → disA_out_g(or(T32, T33))
U1_g(T32, T33, conB_out_g(T32)) → U2_g(T32, T33, disA_in_g(T33))
disA_in_g(T44) → U3_g(T44, conB_in_g(T44))
U3_g(T44, conB_out_g(T44)) → disA_out_g(T44)
U2_g(T32, T33, disA_out_g(T33)) → disA_out_g(or(T32, T33))
U5_g(T14, T15, T5, disA_out_g(T15)) → conB_out_g(and(or(T14, T15), T5))
U5_g(T14, T15, T5, disA_out_g(T15)) → U6_g(T14, T15, T5, conB_in_g(T5))
U6_g(T14, T15, T5, conB_out_g(T5)) → conB_out_g(and(or(T14, T15), T5))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
conB_in_g(and(or(T14, T15), T5)) → U4_g(T14, T15, T5, conB_in_g(T14))
conB_in_g(and(T57, T5)) → U7_g(T57, T5, conB_in_g(T57))
conB_in_g(0) → conB_out_g(0)
conB_in_g(1) → conB_out_g(1)
U7_g(T57, T5, conB_out_g(T57)) → conB_out_g(and(T57, T5))
U7_g(T57, T5, conB_out_g(T57)) → U8_g(T57, T5, conB_in_g(T5))
U8_g(T57, T5, conB_out_g(T5)) → conB_out_g(and(T57, T5))
U4_g(T14, T15, T5, conB_out_g(T14)) → conB_out_g(and(or(T14, T15), T5))
U4_g(T14, T15, T5, conB_out_g(T14)) → U5_g(T14, T15, T5, disA_in_g(T15))
disA_in_g(or(T32, T33)) → U1_g(T32, T33, conB_in_g(T32))
U1_g(T32, T33, conB_out_g(T32)) → disA_out_g(or(T32, T33))
U1_g(T32, T33, conB_out_g(T32)) → U2_g(T32, T33, disA_in_g(T33))
disA_in_g(T44) → U3_g(T44, conB_in_g(T44))
U3_g(T44, conB_out_g(T44)) → disA_out_g(T44)
U2_g(T32, T33, disA_out_g(T33)) → disA_out_g(or(T32, T33))
U5_g(T14, T15, T5, disA_out_g(T15)) → conB_out_g(and(or(T14, T15), T5))
U5_g(T14, T15, T5, disA_out_g(T15)) → U6_g(T14, T15, T5, conB_in_g(T5))
U6_g(T14, T15, T5, conB_out_g(T5)) → conB_out_g(and(or(T14, T15), T5))
CONB_IN_G(and(or(T14, T15), T5)) → U4_G(T14, T15, T5, conB_in_g(T14))
CONB_IN_G(and(or(T14, T15), T5)) → CONB_IN_G(T14)
CONB_IN_G(and(T57, T5)) → U7_G(T57, T5, conB_in_g(T57))
CONB_IN_G(and(T57, T5)) → CONB_IN_G(T57)
U7_G(T57, T5, conB_out_g(T57)) → U8_G(T57, T5, conB_in_g(T5))
U7_G(T57, T5, conB_out_g(T57)) → CONB_IN_G(T5)
U4_G(T14, T15, T5, conB_out_g(T14)) → U5_G(T14, T15, T5, disA_in_g(T15))
U4_G(T14, T15, T5, conB_out_g(T14)) → DISA_IN_G(T15)
DISA_IN_G(or(T32, T33)) → U1_G(T32, T33, conB_in_g(T32))
DISA_IN_G(or(T32, T33)) → CONB_IN_G(T32)
U1_G(T32, T33, conB_out_g(T32)) → U2_G(T32, T33, disA_in_g(T33))
U1_G(T32, T33, conB_out_g(T32)) → DISA_IN_G(T33)
DISA_IN_G(T44) → U3_G(T44, conB_in_g(T44))
DISA_IN_G(T44) → CONB_IN_G(T44)
U5_G(T14, T15, T5, disA_out_g(T15)) → U6_G(T14, T15, T5, conB_in_g(T5))
U5_G(T14, T15, T5, disA_out_g(T15)) → CONB_IN_G(T5)
conB_in_g(and(or(T14, T15), T5)) → U4_g(T14, T15, T5, conB_in_g(T14))
conB_in_g(and(T57, T5)) → U7_g(T57, T5, conB_in_g(T57))
conB_in_g(0) → conB_out_g(0)
conB_in_g(1) → conB_out_g(1)
U7_g(T57, T5, conB_out_g(T57)) → conB_out_g(and(T57, T5))
U7_g(T57, T5, conB_out_g(T57)) → U8_g(T57, T5, conB_in_g(T5))
U8_g(T57, T5, conB_out_g(T5)) → conB_out_g(and(T57, T5))
U4_g(T14, T15, T5, conB_out_g(T14)) → conB_out_g(and(or(T14, T15), T5))
U4_g(T14, T15, T5, conB_out_g(T14)) → U5_g(T14, T15, T5, disA_in_g(T15))
disA_in_g(or(T32, T33)) → U1_g(T32, T33, conB_in_g(T32))
U1_g(T32, T33, conB_out_g(T32)) → disA_out_g(or(T32, T33))
U1_g(T32, T33, conB_out_g(T32)) → U2_g(T32, T33, disA_in_g(T33))
disA_in_g(T44) → U3_g(T44, conB_in_g(T44))
U3_g(T44, conB_out_g(T44)) → disA_out_g(T44)
U2_g(T32, T33, disA_out_g(T33)) → disA_out_g(or(T32, T33))
U5_g(T14, T15, T5, disA_out_g(T15)) → conB_out_g(and(or(T14, T15), T5))
U5_g(T14, T15, T5, disA_out_g(T15)) → U6_g(T14, T15, T5, conB_in_g(T5))
U6_g(T14, T15, T5, conB_out_g(T5)) → conB_out_g(and(or(T14, T15), T5))
CONB_IN_G(and(or(T14, T15), T5)) → U4_G(T14, T15, T5, conB_in_g(T14))
CONB_IN_G(and(or(T14, T15), T5)) → CONB_IN_G(T14)
CONB_IN_G(and(T57, T5)) → U7_G(T57, T5, conB_in_g(T57))
CONB_IN_G(and(T57, T5)) → CONB_IN_G(T57)
U7_G(T57, T5, conB_out_g(T57)) → U8_G(T57, T5, conB_in_g(T5))
U7_G(T57, T5, conB_out_g(T57)) → CONB_IN_G(T5)
U4_G(T14, T15, T5, conB_out_g(T14)) → U5_G(T14, T15, T5, disA_in_g(T15))
U4_G(T14, T15, T5, conB_out_g(T14)) → DISA_IN_G(T15)
DISA_IN_G(or(T32, T33)) → U1_G(T32, T33, conB_in_g(T32))
DISA_IN_G(or(T32, T33)) → CONB_IN_G(T32)
U1_G(T32, T33, conB_out_g(T32)) → U2_G(T32, T33, disA_in_g(T33))
U1_G(T32, T33, conB_out_g(T32)) → DISA_IN_G(T33)
DISA_IN_G(T44) → U3_G(T44, conB_in_g(T44))
DISA_IN_G(T44) → CONB_IN_G(T44)
U5_G(T14, T15, T5, disA_out_g(T15)) → U6_G(T14, T15, T5, conB_in_g(T5))
U5_G(T14, T15, T5, disA_out_g(T15)) → CONB_IN_G(T5)
conB_in_g(and(or(T14, T15), T5)) → U4_g(T14, T15, T5, conB_in_g(T14))
conB_in_g(and(T57, T5)) → U7_g(T57, T5, conB_in_g(T57))
conB_in_g(0) → conB_out_g(0)
conB_in_g(1) → conB_out_g(1)
U7_g(T57, T5, conB_out_g(T57)) → conB_out_g(and(T57, T5))
U7_g(T57, T5, conB_out_g(T57)) → U8_g(T57, T5, conB_in_g(T5))
U8_g(T57, T5, conB_out_g(T5)) → conB_out_g(and(T57, T5))
U4_g(T14, T15, T5, conB_out_g(T14)) → conB_out_g(and(or(T14, T15), T5))
U4_g(T14, T15, T5, conB_out_g(T14)) → U5_g(T14, T15, T5, disA_in_g(T15))
disA_in_g(or(T32, T33)) → U1_g(T32, T33, conB_in_g(T32))
U1_g(T32, T33, conB_out_g(T32)) → disA_out_g(or(T32, T33))
U1_g(T32, T33, conB_out_g(T32)) → U2_g(T32, T33, disA_in_g(T33))
disA_in_g(T44) → U3_g(T44, conB_in_g(T44))
U3_g(T44, conB_out_g(T44)) → disA_out_g(T44)
U2_g(T32, T33, disA_out_g(T33)) → disA_out_g(or(T32, T33))
U5_g(T14, T15, T5, disA_out_g(T15)) → conB_out_g(and(or(T14, T15), T5))
U5_g(T14, T15, T5, disA_out_g(T15)) → U6_g(T14, T15, T5, conB_in_g(T5))
U6_g(T14, T15, T5, conB_out_g(T5)) → conB_out_g(and(or(T14, T15), T5))
U4_G(T14, T15, T5, conB_out_g(T14)) → U5_G(T14, T15, T5, disA_in_g(T15))
U5_G(T14, T15, T5, disA_out_g(T15)) → CONB_IN_G(T5)
CONB_IN_G(and(or(T14, T15), T5)) → U4_G(T14, T15, T5, conB_in_g(T14))
U4_G(T14, T15, T5, conB_out_g(T14)) → DISA_IN_G(T15)
DISA_IN_G(or(T32, T33)) → U1_G(T32, T33, conB_in_g(T32))
U1_G(T32, T33, conB_out_g(T32)) → DISA_IN_G(T33)
DISA_IN_G(or(T32, T33)) → CONB_IN_G(T32)
CONB_IN_G(and(or(T14, T15), T5)) → CONB_IN_G(T14)
CONB_IN_G(and(T57, T5)) → U7_G(T57, T5, conB_in_g(T57))
U7_G(T57, T5, conB_out_g(T57)) → CONB_IN_G(T5)
CONB_IN_G(and(T57, T5)) → CONB_IN_G(T57)
DISA_IN_G(T44) → CONB_IN_G(T44)
conB_in_g(and(or(T14, T15), T5)) → U4_g(T14, T15, T5, conB_in_g(T14))
conB_in_g(and(T57, T5)) → U7_g(T57, T5, conB_in_g(T57))
conB_in_g(0) → conB_out_g(0)
conB_in_g(1) → conB_out_g(1)
U7_g(T57, T5, conB_out_g(T57)) → conB_out_g(and(T57, T5))
U7_g(T57, T5, conB_out_g(T57)) → U8_g(T57, T5, conB_in_g(T5))
U8_g(T57, T5, conB_out_g(T5)) → conB_out_g(and(T57, T5))
U4_g(T14, T15, T5, conB_out_g(T14)) → conB_out_g(and(or(T14, T15), T5))
U4_g(T14, T15, T5, conB_out_g(T14)) → U5_g(T14, T15, T5, disA_in_g(T15))
disA_in_g(or(T32, T33)) → U1_g(T32, T33, conB_in_g(T32))
U1_g(T32, T33, conB_out_g(T32)) → disA_out_g(or(T32, T33))
U1_g(T32, T33, conB_out_g(T32)) → U2_g(T32, T33, disA_in_g(T33))
disA_in_g(T44) → U3_g(T44, conB_in_g(T44))
U3_g(T44, conB_out_g(T44)) → disA_out_g(T44)
U2_g(T32, T33, disA_out_g(T33)) → disA_out_g(or(T32, T33))
U5_g(T14, T15, T5, disA_out_g(T15)) → conB_out_g(and(or(T14, T15), T5))
U5_g(T14, T15, T5, disA_out_g(T15)) → U6_g(T14, T15, T5, conB_in_g(T5))
U6_g(T14, T15, T5, conB_out_g(T5)) → conB_out_g(and(or(T14, T15), T5))
U4_G(T15, T5, conB_out_g) → U5_G(T5, disA_in_g(T15))
U5_G(T5, disA_out_g) → CONB_IN_G(T5)
CONB_IN_G(and(or(T14, T15), T5)) → U4_G(T15, T5, conB_in_g(T14))
U4_G(T15, T5, conB_out_g) → DISA_IN_G(T15)
DISA_IN_G(or(T32, T33)) → U1_G(T33, conB_in_g(T32))
U1_G(T33, conB_out_g) → DISA_IN_G(T33)
DISA_IN_G(or(T32, T33)) → CONB_IN_G(T32)
CONB_IN_G(and(or(T14, T15), T5)) → CONB_IN_G(T14)
CONB_IN_G(and(T57, T5)) → U7_G(T5, conB_in_g(T57))
U7_G(T5, conB_out_g) → CONB_IN_G(T5)
CONB_IN_G(and(T57, T5)) → CONB_IN_G(T57)
DISA_IN_G(T44) → CONB_IN_G(T44)
conB_in_g(and(or(T14, T15), T5)) → U4_g(T15, T5, conB_in_g(T14))
conB_in_g(and(T57, T5)) → U7_g(T5, conB_in_g(T57))
conB_in_g(0) → conB_out_g
conB_in_g(1) → conB_out_g
U7_g(T5, conB_out_g) → conB_out_g
U7_g(T5, conB_out_g) → U8_g(conB_in_g(T5))
U8_g(conB_out_g) → conB_out_g
U4_g(T15, T5, conB_out_g) → conB_out_g
U4_g(T15, T5, conB_out_g) → U5_g(T5, disA_in_g(T15))
disA_in_g(or(T32, T33)) → U1_g(T33, conB_in_g(T32))
U1_g(T33, conB_out_g) → disA_out_g
U1_g(T33, conB_out_g) → U2_g(disA_in_g(T33))
disA_in_g(T44) → U3_g(conB_in_g(T44))
U3_g(conB_out_g) → disA_out_g
U2_g(disA_out_g) → disA_out_g
U5_g(T5, disA_out_g) → conB_out_g
U5_g(T5, disA_out_g) → U6_g(conB_in_g(T5))
U6_g(conB_out_g) → conB_out_g
conB_in_g(x0)
U7_g(x0, x1)
U8_g(x0)
U4_g(x0, x1, x2)
disA_in_g(x0)
U1_g(x0, x1)
U3_g(x0)
U2_g(x0)
U5_g(x0, x1)
U6_g(x0)
From the DPs we obtained the following set of size-change graphs: